TeX Snippet Sources

\documentclass[a4paper]{scrartcl}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amsthm}
\usepackage{cite}
\usepackage{url}
\usepackage{eulervm}
\usepackage{version}
\usepackage{mathpartir}
\usepackage{haskell,grammar,alltt}
\usepackage{tcolorbox}

\title{COMP3161/9164 23T3 Assignment 0\\
       Latex Snippets}

% \date{}

\begin{document}

\maketitle

\section{Purpose}
This document quotes the \LaTeX source of some of the assignment spec document,
both as a guide and example, and so that you can use the same fonts and styles
for math terms in your answers as used in the questions.

There will be marks won or lots for purely aesthetic concerns such as using the
same fonts as in the question.

\subsection*{Part A}

The language of boolean expressions $\mathcal{P}$ contains terms such as:
$$ \{ \mathtt{True}, \mathtt{False}, \neg \mathtt{True}, \neg \mathtt{False}, \mathtt{True} \wedge \mathtt{False},  \neg(\mathtt{True} \wedge \mathtt{False}), \dots \} $$


The \emph{abstract syntax} of $\mathcal{B}$ contains:
          $$ \mathcal{B} ::= \mathsf{Not}\ \mathcal{B}\ |\ \mathsf{And}\ \mathcal{B}\ \mathcal{B}\ |\ \mathsf{True}\ |\ \mathsf{False} $$

The big-step semantics of $\mathcal{B}$ is defined by:
          \begin{gather*}
             \inferrule{ x \Downarrow \mathsf{True} }{\mathsf{Not}\ x \Downarrow \mathsf{False}}(\textsc{N}_1)\quad
             \inferrule{ x \Downarrow \mathsf{False } }{\mathsf{Not}\ x \Downarrow \mathsf{True}}(\textsc{N}_2)\quad
             \inferrule{ \quad }{ \mathsf{True} \Downarrow \mathsf{True} }(\textsc{N}_3)\quad
             \inferrule{ \quad }{ \mathsf{False} \Downarrow \mathsf{False} }(\textsc{N}_4) \\
             \inferrule{ x \Downarrow \mathsf{False} }{\mathsf{And}\ x\ y \Downarrow \mathsf{False}}(\textsc{N}_5)\quad
             \inferrule{ x \Downarrow \mathsf{True} \quad y \Downarrow v}{\mathsf{And}\ x\ y \Downarrow v}(\textsc{N}_6)
          \end{gather*}

There is a question about $v^{-1}$, understood to be defined by the following equations:
          \[
          \begin{array}{lcl}
            \mathsf{True}^{-1} = \mathsf{False} \\
            \mathsf{False}^{-1} = \mathsf{True}
          \end{array}
          \]

\subsection*{Stacking Natural Deduction}

Here is, as an example, one of the derivations of
$1 \times 2 \times 3\ \mathbf{PExp}$ from Week 2's slides:

        $$
            \inferrule{\inferrule{\inferrule{1 \in \mathbb{Z}}{1\ \mathbf{Atom}}}{1\ \mathbf{PExp}}
                    \quad \inferrule{\inferrule{\inferrule{2 \in \mathbb{Z}}{2\ \mathbf{Atom}}}{2\ \mathbf{PExp}}
                               \quad \inferrule{\inferrule{3 \in \mathbb{Z}}{3\ \mathbf{Atom}}}{3\ \mathbf{PExp}}}
                                 {2 \times 3\ \mathbf{PExp}}}
                      {1 \times 2 \times 3\ \mathbf{PExp}}
        $$

\subsection*{Part B}

The small-step for $\mathcal{L}$ is characterised by the rules:
\begin{gather*}
    \inferrule{ c \mapsto c' }{(\texttt{If}\ c\ t\ e) \mapsto (\texttt{If}\ c'\ t\ e) }(1)\quad
    \inferrule{ }{(\texttt{If}\ \texttt{True}\ t\ e) \mapsto t }(2)\quad
    \inferrule{ }{(\texttt{If}\ \texttt{False}\ t\ e) \mapsto e }(3)
\end{gather*}


The question is about $e \Downarrow v$ and $e \stackrel{\star}{\mapsto} v$.




\subsection*{Part D}

Here is a term in $\lambda$-calculus:
$$ (\lambda n.\ \lambda f.\ \lambda x.\ (n\ f\ (f\ x)))\ (\lambda f.\ \lambda x.\ f\ x) $$


The question is about $\beta$-reduction and $\eta$-reduction.

\subsection*{Part E}

Here's some concrete syntax:
  \[
  \begin{array}{l}
    \mathsf{let} \\
    \;\;\mathit{g}(\mathit{x}) = \neg\mathit{x} \\
    \mathsf{in} \\
    \;\; \mathit{g}(\mathsf{True})\\
    \mathsf{end}
  \end{array}
  \]

\end{document}